SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Formal methods</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Formal methods</span></span>

</h1>

</header>

<p>In <a href="Computer_science" title="Computer science">computer science</a>, <b>formal methods</b> are <a href="Mathematics" title="Mathematics">mathematically</a> rigorous techniques for the <a href="Formal_specification" title="Formal specification">specification</a>, development, <a href="Program_analysis" title="Program analysis">analysis</a>, and <a href="Formal_verification" title="Formal verification">verification</a> of <a href="Software" title="Software">software</a> and <a href="Computer_hardware" title="Computer hardware">hardware</a> systems.<sup id="cite_ref-butler_1-0" class="reference"><a href="#cite_note-butler-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p><p>Formal methods employ a variety of <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a> fundamentals, including <a href="Logic_in_computer_science" title="Logic in computer science">logic</a> calculi, <a href="Formal_language" title="Formal language">formal languages</a>, <a href="Automata_theory" title="Automata theory">automata theory</a>, <a href="Control_theory" title="Control theory">control theory</a>, <a href="Program_semantics" class="mw-redirect" title="Program semantics">program semantics</a>, <a href="Type_systems" class="mw-redirect" title="Type systems">type systems</a>, and <a href="Type_theory" title="Type theory">type theory</a>.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p>

<p>Formal methods can be applied at various points through the <a href="Software_development_process" title="Software development process">development process</a>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Specification">Specification</h3></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_specification" title="Formal specification">Formal specification</a></div>

<p>Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system.

</p><p>Alternatively, specification may be the only stage in which formal methods is used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>

</p><p>The need for formal specification systems has been noted for years. In the <a href="ALGOL_58" title="ALGOL 58">ALGOL 58</a> report,<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> <a href="John_Backus" title="John Backus">John Backus</a> presented a formal notation for describing <a href="Syntax_(programming_languages)" title="Syntax (programming languages)">programming language syntax</a>, later named <a href="Backus_normal_form" class="mw-redirect" title="Backus normal form">Backus normal form</a> then renamed <a href="Backus%E2%80%93Naur_form" title="Backus–Naur form">Backus–Naur form</a> (BNF).<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="Synthesis">Synthesis</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Program_synthesis" title="Program synthesis">Program synthesis</a></div>

<p>Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="Verification">Verification</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_verification" title="Formal verification">Formal verification</a></div>

<p>Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system <a href="Implementation" title="Implementation">implementation</a> satisfies its specification.

</p><p>Once a formal specification has been developed, the specification may be used as the basis for <a href="Mathematical_proof" title="Mathematical proof">proving</a> properties of the specification, and by inference, properties of the system implementation.

</p>

<div class="mw-heading mw-heading4"><h4 id="Sign-off_verification">Sign-off verification</h4></div>

<p>Sign-off verification is the use of a formal verification tool that is highly trusted. Such a tool can replace traditional verification methods (the tool may even be certified).

</p>

<div class="mw-heading mw-heading4"><h4 id="Human-directed_proof">Human-directed proof</h4></div>

<p>Sometimes, the motivation for proving the <a href="Correctness_(computer_science)" title="Correctness (computer science)">correctness</a> of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of <a href="Mathematical_proof" title="Mathematical proof">mathematical proof</a>: handwritten (or typeset) using <a href="Natural_language" title="Natural language">natural language</a>, using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers.

</p><p>Critics of such approaches point out that the <a href="Ambiguity" title="Ambiguity">ambiguity</a> inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

</p>

<div class="mw-heading mw-heading4"><h4 id="Automated_proof">Automated proof</h4></div>

<p>In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:

</p>

<ul><li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a>, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical <a href="Axiom" title="Axiom">axioms</a>, and a set of <a href="Rule_of_inference" title="Rule of inference">inference rules</a>.</li>

<li><a href="Model_checking" title="Model checking">Model checking</a>, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.</li>

<li><a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a>, in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) <a href="Lattice_(order_theory)" class="mw-redirect" title="Lattice (order theory)">lattice</a> representing it.</li></ul>

<p>Some <a href="Automated_theorem_proving" title="Automated theorem proving">automated theorem provers</a> require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.

</p><p>Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.

</p><p>Critics note that some of those systems are like <a href="Oracle_machine" title="Oracle machine">oracles</a>: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "<a href="Quis_custodiet_ipsos_custodes%3F" title="Quis custodiet ipsos custodes?">verifying the verifier</a>"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.

</p><p>The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> to get fast convergence.

</p>

<div class="mw-heading mw-heading2"><h2 id="Techniques">Techniques</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p>Formal methods includes a number of different techniques.

</p>

<div class="mw-heading mw-heading3"><h3 id="Specification_languages">Specification languages</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Specification_language" title="Specification language">Specification language</a></div>

<p>The design of a computing system can be expressed using a specification language, which is a formal language that includes a proof system. Using this proof system, formal verification tools can reason about the specification and establish that a system adheres to the specification.<sup id="cite_ref-10" class="reference"><a href="#cite_note-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="Binary_decision_diagrams">Binary decision diagrams</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Binary_decision_diagram" title="Binary decision diagram">Binary decision diagram</a></div>

<p>A binary decision diagram is a data structure that represents a <a href="Boolean_function" title="Boolean function">Boolean function</a>.<sup id="cite_ref-11" class="reference"><a href="#cite_note-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> If a Boolean formula <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {P}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {P}}}</annotation>

</semantics>

</math></span><img src="./10d6ec962de5797ba4f161c40e66dca74ae95cc6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.704ex; height:2.176ex;" alt="{\displaystyle {\mathcal {P}}}" loading="lazy"></span> expresses that an execution of a program conforms to the specification, a binary decision diagram can be used to determine if <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {P}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {P}}}</annotation>

</semantics>

</math></span><img src="./10d6ec962de5797ba4f161c40e66dca74ae95cc6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.704ex; height:2.176ex;" alt="{\displaystyle {\mathcal {P}}}" loading="lazy"></span> is a tautology; that is, it always evaluates to TRUE. If this is the case, then the program always conforms to the specification.<sup id="cite_ref-12" class="reference"><a href="#cite_note-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="SAT_solvers">SAT solvers</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="SAT_solver" title="SAT solver">SAT solver</a></div>

<p>A SAT solver is a program that can solve the <a href="Boolean_satisfiability_problem" title="Boolean satisfiability problem">Boolean satisfiability problem</a>, the problem of finding an assignment of variables that makes a given propositional formula evaluate to true. If a Boolean formula <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {P}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {P}}}</annotation>

</semantics>

</math></span><img src="./10d6ec962de5797ba4f161c40e66dca74ae95cc6.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.704ex; height:2.176ex;" alt="{\displaystyle {\mathcal {P}}}" loading="lazy"></span> expresses that a specific execution of a program conforms to the specification, then determining that <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg {\mathcal {P}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg {\mathcal {P}}}</annotation>

</semantics>

</math></span><img src="./73e9185bf9e50e1daf86e340da72ad0e2b10f3d0.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:3.254ex; height:2.176ex;" alt="{\displaystyle \neg {\mathcal {P}}}" loading="lazy"></span> is unsatisfiable is equivalent to determining that all executions conform to the specification. SAT solvers are often used in bounded model checking, but can also be used in unbounded model checking.<sup id="cite_ref-13" class="reference"><a href="#cite_note-13"><span class="cite-bracket">[</span>13<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Applications">Applications</h2></div>

<p>Formal methods are applied in different areas of hardware and software, including <a href="Router_(computing)" title="Router (computing)">routers</a>, <a href="Ethernet_switches" class="mw-redirect" title="Ethernet switches">Ethernet switches</a>, <a href="Routing_protocol" title="Routing protocol">routing protocols</a>, security applications, and <a href="Operating_system" title="Operating system">operating system</a> <a href="Microkernel" title="Microkernel">microkernels</a> such as <a href="SeL4" class="mw-redirect" title="SeL4">seL4</a>. There are several examples in which they have been used to verify the functionality of the hardware and software used in <a href="Data_centre" class="mw-redirect" title="Data centre">data centres</a>. <a href="IBM" title="IBM">IBM</a> used <a href="ACL2" title="ACL2">ACL2</a>, a theorem prover, in the <a href="AMD" title="AMD">AMD</a> x86 processor development process. Intel uses such methods to verify its hardware and <a href="Firmware" title="Firmware">firmware</a> (permanent software programmed into a <a href="Read-only_memory" title="Read-only memory">read-only memory</a>). <a href="Dansk_Datamatik_Center" title="Dansk Datamatik Center">Dansk Datamatik Center</a> used formal methods in the 1980s to develop a compiler system for the <a href="Ada_programming_language" class="mw-redirect" title="Ada programming language">Ada programming language</a> that went on to become a long-lived commercial product.<sup id="cite_ref-14" class="reference"><a href="#cite_note-14"><span class="cite-bracket">[</span>14<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-15" class="reference"><a href="#cite_note-15"><span class="cite-bracket">[</span>15<span class="cite-bracket">]</span></a></sup>

</p><p>There are several other projects of <a href="NASA" title="NASA">NASA</a> in which formal methods are applied, such as <a href="Next_Generation_Air_Transportation_System" title="Next Generation Air Transportation System">Next Generation Air Transportation System</a>, Unmanned Aircraft System integration in National Airspace System,<sup id="cite_ref-16" class="reference"><a href="#cite_note-16"><span class="cite-bracket">[</span>16<span class="cite-bracket">]</span></a></sup> and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).<sup id="cite_ref-17" class="reference"><a href="#cite_note-17"><span class="cite-bracket">[</span>17<span class="cite-bracket">]</span></a></sup>

<a href="B-Method" title="B-Method">B-Method</a> with <a href="Atelier_B" class="mw-redirect" title="Atelier B">Atelier B</a>,<sup id="cite_ref-18" class="reference"><a href="#cite_note-18"><span class="cite-bracket">[</span>18<span class="cite-bracket">]</span></a></sup> is used to develop safety automatisms for the various subways installed throughout the world by <a href="Alstom" title="Alstom">Alstom</a> and <a href="Siemens" title="Siemens">Siemens</a>, and also for <a href="Common_Criteria" title="Common Criteria">Common Criteria</a> certification and the development of system models by <a href="ATMEL" class="mw-redirect" title="ATMEL">ATMEL</a> and <a href="STMicroelectronics" title="STMicroelectronics">STMicroelectronics</a>.

</p><p>Formal verification has been frequently used in hardware by most of the well-known hardware vendors, such as IBM, <a href="Intel" title="Intel">Intel</a>, and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache-coherent protocol,<sup id="cite_ref-19" class="reference"><a href="#cite_note-19"><span class="cite-bracket">[</span>19<span class="cite-bracket">]</span></a></sup> Intel Core i7 processor execution engine validation <sup id="cite_ref-20" class="reference"><a href="#cite_note-20"><span class="cite-bracket">[</span>20<span class="cite-bracket">]</span></a></sup> (using theorem proving, <a href="Binary_decision_diagram" title="Binary decision diagram">BDDs</a>, and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,<sup id="cite_ref-21" class="reference"><a href="#cite_note-21"><span class="cite-bracket">[</span>21<span class="cite-bracket">]</span></a></sup> and verification of high-performance dual-port <a href="Gigabit_Ethernet" title="Gigabit Ethernet">gigabit Ethernet</a> <a href="Network_interface_controller" title="Network interface controller">controller</a> with support for <a href="PCI_Express" title="PCI Express">PCI express</a> protocol and Intel advance management technology using Cadence.<sup id="cite_ref-22" class="reference"><a href="#cite_note-22"><span class="cite-bracket">[</span>22<span class="cite-bracket">]</span></a></sup> Similarly, IBM has used formal methods in the verification of power gates,<sup id="cite_ref-23" class="reference"><a href="#cite_note-23"><span class="cite-bracket">[</span>23<span class="cite-bracket">]</span></a></sup> registers,<sup id="cite_ref-24" class="reference"><a href="#cite_note-24"><span class="cite-bracket">[</span>24<span class="cite-bracket">]</span></a></sup> and functional verification of the IBM Power7 microprocessor.<sup id="cite_ref-25" class="reference"><a href="#cite_note-25"><span class="cite-bracket">[</span>25<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="In_software_development">In software development</h2></div>

<p>In <a href="Software_development" title="Software development">software development</a>, formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety-critical or security-critical software and systems, such as <a href="Avionics_software" title="Avionics software">avionics software</a>. Software safety assurance standards, such as <a href="DO-178C" title="DO-178C">DO-178C</a> allows the usage of formal methods through supplementation, and <a href="Common_Criteria" title="Common Criteria">Common Criteria</a> mandates formal methods at the highest levels of categorization.

</p><p>For sequential software, examples of formal methods include the <a href="B-Method" title="B-Method">B-Method</a>, the specification languages used in <a href="Automated_theorem_proving" title="Automated theorem proving">automated theorem proving</a>, <a href="Rigorous_Approach_to_Industrial_Software_Engineering" title="Rigorous Approach to Industrial Software Engineering">RAISE</a>, and the <a href="Z_notation" title="Z notation">Z notation</a>.

</p><p>In <a href="Functional_programming" title="Functional programming">functional programming</a>, <a href="QuickCheck" title="QuickCheck">property-based testing</a> has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions.

</p><p>The <a href="Object_Constraint_Language" title="Object Constraint Language">Object Constraint Language</a> (and specializations such as <a href="Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a>) has allowed object-oriented systems to be formally specified, if not necessarily formally verified.

</p><p>For concurrent software and systems, <a href="Petri_net" title="Petri net">Petri nets</a>, <a href="Process_algebra" class="mw-redirect" title="Process algebra">process algebra</a>, and <a href="Finite-state_machine" title="Finite-state machine">finite-state machines</a> (which are based on <a href="Automata_theory" title="Automata theory">automata theory</a>; see also <a href="Virtual_finite_state_machine" class="mw-redirect" title="Virtual finite state machine">virtual finite state machine</a> or <a href="Event_driven_finite_state_machine" class="mw-redirect" title="Event driven finite state machine">event driven finite state machine</a>) allow executable software specification and can be used to build up and validate application behaviour.

</p><p>Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of <a href="First-order_logic" title="First-order logic">first-order logic</a>—and then to directly execute the logic as though it were a program. The <a href="Web_Ontology_Language" title="Web Ontology Language">OWL</a> language, based on <a href="Description_logic" title="Description logic">description logic</a>, is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are <a href="Attempto_Controlled_English" title="Attempto Controlled English">Attempto Controlled English</a>, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.

</p>

<div class="mw-heading mw-heading2"><h2 id="Semi-formal_methods">Semi-formal methods</h2></div>

<p>Semi-formal methods are formalisms and languages that are not considered fully "formal". It defers the task of completing the semantics to a later stage, which is then done either by human interpretation or by interpretation through software like code or test case <a href="Generator_(computer_programming)" title="Generator (computer programming)">generators</a>.<sup id="cite_ref-26" class="reference"><a href="#cite_note-26"><span class="cite-bracket">[</span>26<span class="cite-bracket">]</span></a></sup>

</p><p>Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.<sup id="cite_ref-27" class="reference"><a href="#cite_note-27"><span class="cite-bracket">[</span>27<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-28" class="reference"><a href="#cite_note-28"><span class="cite-bracket">[</span>28<span class="cite-bracket">]</span></a></sup> They contend that the <a href="Expressive_power_(computer_science)" title="Expressive power (computer science)">expressiveness</a> of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various <i>lightweight</i> formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the <a href="Alloy_language" class="mw-redirect" title="Alloy language">Alloy</a> object modelling notation,<sup id="cite_ref-29" class="reference"><a href="#cite_note-29"><span class="cite-bracket">[</span>29<span class="cite-bracket">]</span></a></sup> Denney's synthesis of some aspects of the <a href="Z_notation" title="Z notation">Z notation</a> with <a href="Use_case" title="Use case">use case</a> driven development,<sup id="cite_ref-30" class="reference"><a href="#cite_note-30"><span class="cite-bracket">[</span>30<span class="cite-bracket">]</span></a></sup> and the CSK <a href="Vienna_Development_Method" title="Vienna Development Method">VDM</a> Tools.<sup id="cite_ref-31" class="reference"><a href="#cite_note-31"><span class="cite-bracket">[</span>31<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Formal_methods_and_notations">Formal methods and notations</h2></div>

<p>There are a variety of formal methods and notations available.

</p>

<div class="mw-heading mw-heading3"><h3 id="Specification_languages_2">Specification languages</h3></div>

<ul><li><a href="Abstract_State_Machines" class="mw-redirect" title="Abstract State Machines">Abstract State Machines</a> (ASMs)</li>

<li><a href="ACL2" title="ACL2">A Computational Logic for Applicative Common Lisp</a> (ACL2)</li>

<li><a href="Actor_model" title="Actor model">Actor model</a></li>

<li><a href="Alloy_language" class="mw-redirect" title="Alloy language">Alloy</a></li>

<li><a href="ANSI/ISO_C_Specification_Language" title="ANSI/ISO C Specification Language">ANSI/ISO C Specification Language</a> (ACSL)</li>

<li><a href="Autonomic_System_Specification_Language" class="mw-redirect" title="Autonomic System Specification Language">Autonomic System Specification Language</a> (ASSL)</li>

<li><a href="B-Method" title="B-Method">B-Method</a></li>

<li><a href="Common_Algebraic_Specification_Language" title="Common Algebraic Specification Language">Common Algebraic Specification Language</a> (CASL)</li>

<li><a href="Esterel" title="Esterel">Esterel</a></li>

<li><a href="Java_Modeling_Language" title="Java Modeling Language">Java Modeling Language</a> (JML)</li>

<li><a href="Knowledge_Based_Software_Assistant" title="Knowledge Based Software Assistant">Knowledge Based Software Assistant</a> (KBSA)</li>

<li><a href="Lustre_programming_language" class="mw-redirect" title="Lustre programming language">Lustre</a></li>

<li><a href="Perfect_Developer" title="Perfect Developer">Perfect Developer</a></li>

<li><a href="Petri_nets" class="mw-redirect" title="Petri nets">Petri nets</a></li>

<li><a href="Predicative_programming" title="Predicative programming">Predicative programming</a></li>

<li><a href="Process_calculi" class="mw-redirect" title="Process calculi">Process calculi</a>

<li><a href="Language_Of_Temporal_Ordering_Specification" class="mw-redirect" title="Language Of Temporal Ordering Specification">LOTOS</a></li>

<li><a href="Pi-calculus" class="mw-redirect" title="Pi-calculus">π-calculus</a></li></ul></li>

<li><a href="RAISE_specification_language" class="mw-redirect" title="RAISE specification language">RAISE</a></li>

<li><a href="Rebeca_Modeling_Language" class="mw-redirect" title="Rebeca Modeling Language">Rebeca Modeling Language</a></li>

<li><a href="SPARK_(programming_language)" title="SPARK (programming language)">SPARK Ada</a></li>

<li><a href="Specification_and_Description_Language" title="Specification and Description Language">Specification and Description Language</a></li>

<li><a href="Z_notation" title="Z notation">Z notation</a></li></ul>

<div class="mw-heading mw-heading3"><h3 id="Model_checkers">Model checkers</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="List_of_model_checking_tools" title="List of model checking tools">List of model checking tools</a></div>

<ul><li>ESBMC<sup id="cite_ref-32" class="reference"><a href="#cite_note-32"><span class="cite-bracket">[</span>32<span class="cite-bracket">]</span></a></sup></li>

<li><a href="MALPAS_Software_Static_Analysis_Toolset" title="MALPAS Software Static Analysis Toolset">MALPAS Software Static Analysis Toolset</a> – an industrial-strength model checker used for formal proof of safety-critical systems</li>

<li><a href="PAT_(model_checker)" title="PAT (model checker)">PAT</a> – a free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g., shared variables, arrays, fairness)</li>

<li><a href="Uppaal_Model_Checker" title="Uppaal Model Checker">UPPAAL</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Solvers_and_competitions">Solvers and competitions</h2></div>

<p>Many problems in formal methods are <a href="NP-hardness" title="NP-hardness">NP-hard</a>, but can be solved in cases arising in practice. For example, the Boolean satisfiability problem is <a href="NP-completeness" title="NP-completeness">NP-complete</a> by the <a href="Cook%E2%80%93Levin_theorem" title="Cook–Levin theorem">Cook–Levin theorem</a>, but <a href="SAT_solver" title="SAT solver">SAT solvers</a> can solve a variety of large instances. There are "solvers" for a variety of problems that arise in formal methods, and there are many periodic competitions to evaluate the state-of-the-art in solving such problems.<sup id="cite_ref-33" class="reference"><a href="#cite_note-33"><span class="cite-bracket">[</span>33<span class="cite-bracket">]</span></a></sup>

</p>

<ul><li>The SAT competition is a yearly competition that compares SAT solvers.<sup id="cite_ref-34" class="reference"><a href="#cite_note-34"><span class="cite-bracket">[</span>34<span class="cite-bracket">]</span></a></sup> SAT solvers are used in formal methods tools such as <a href="Alloy_(specification_language)" title="Alloy (specification language)">Alloy</a>.<sup id="cite_ref-35" class="reference"><a href="#cite_note-35"><span class="cite-bracket">[</span>35<span class="cite-bracket">]</span></a></sup></li>

<li><a href="CADE_ATP_System_Competition" title="CADE ATP System Competition">CASC</a> is a yearly competition of <a href="Automated_theorem_prover" class="mw-redirect" title="Automated theorem prover">automated theorem provers</a>.</li>

<li><a href="SMT-COMP" class="mw-redirect" title="SMT-COMP">SMT-COMP</a> is a yearly competition of <a href="SMT_solver" class="mw-redirect" title="SMT solver">SMT solvers</a>, which are applied to <a href="Formal_verification" title="Formal verification">formal verification</a>.<sup id="cite_ref-36" class="reference"><a href="#cite_note-36"><span class="cite-bracket">[</span>36<span class="cite-bracket">]</span></a></sup></li>

<li><a href="CHC-COMP" class="mw-redirect" title="CHC-COMP">CHC-COMP</a> is a yearly competition of solvers of <a href="Constrained_Horn_clauses" title="Constrained Horn clauses">constrained Horn clauses</a>, which have applications to formal verification.<sup id="cite_ref-37" class="reference"><a href="#cite_note-37"><span class="cite-bracket">[</span>37<span class="cite-bracket">]</span></a></sup></li>

<li><a href="QBFEVAL" class="mw-redirect" title="QBFEVAL">QBFEVAL</a> is a biennial competition of solvers for <a href="True_quantified_Boolean_formula" title="True quantified Boolean formula">true quantified Boolean formulas</a>, which have applications to <a href="Model_checking" title="Model checking">model checking</a>.<sup id="cite_ref-38" class="reference"><a href="#cite_note-38"><span class="cite-bracket">[</span>38<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-39" class="reference"><a href="#cite_note-39"><span class="cite-bracket">[</span>39<span class="cite-bracket">]</span></a></sup></li>

<li>SV-COMP is an annual competition for software verification tools.<sup id="cite_ref-40" class="reference"><a href="#cite_note-40"><span class="cite-bracket">[</span>40<span class="cite-bracket">]</span></a></sup></li>

<li><a href="SyGuS-COMP" class="mw-redirect" title="SyGuS-COMP">SyGuS-COMP</a> is an annual competition for <a href="Program_synthesis" title="Program synthesis">program synthesis</a> tools.<sup id="cite_ref-41" class="reference"><a href="#cite_note-41"><span class="cite-bracket">[</span>41<span class="cite-bracket">]</span></a></sup></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Organizations">Organizations</h2></div>

<li><a href="Formal_Methods_Europe" title="Formal Methods Europe">Formal Methods Europe</a></li>

<li><a href="Z_User_Group" title="Z User Group">Z User Group</a></li></ul>

<ul><li><a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a></li>

<li><a href="Automated_theorem_proving" title="Automated theorem proving">Automated theorem proving</a></li>

<li><a href="Design_by_contract" title="Design by contract">Design by contract</a></li>

<li>Formal methods people</li>

<li><a href="Formal_science" title="Formal science">Formal science</a></li>

<li><a href="Formal_specification" title="Formal specification">Formal specification</a></li>

<li><a href="Formal_verification" title="Formal verification">Formal verification</a></li>

<li><a href="Formal_system" title="Formal system">Formal system</a></li>

<li><a href="Methodism" title="Methodism">Methodism</a></li>

<li><a href="Methodology" title="Methodology">Methodology</a></li>

<li><a href="Model_checking" title="Model checking">Model checking</a></li>

<li><a href="Scientific_method" title="Scientific method">Scientific method</a></li>

<li><a href="Software_engineering" title="Software engineering">Software engineering</a></li>

<li><a href="Specification_language" title="Specification language">Specification language</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFButler2001" class="citation web cs1">Butler, R. W. (2001-08-06). <a rel="nofollow" class="external text" href="https://shemesh.larc.nasa.gov/fm/fm-what.html">"What is Formal Methods?"</a><span class="reference-accessdate">. Retrieved <span class="nowrap">2006-11-16</span></span>.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFHolloway" class="citation journal cs1">Holloway, C. Michael. <a rel="nofollow" class="external text" href="https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf">"Why Engineers Should Consider Formal Methods"</a> <span class="cs1-format">(PDF)</span>. 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from <a rel="nofollow" class="external text" href="http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf">the original</a> <span class="cs1-format">(PDF)</span> on 16 November 2006<span class="reference-accessdate">. Retrieved <span class="nowrap">2006-11-16</span></span>.</cite> <span class="cs1-visible-error citation-comment"><code class="cs1-code">{{cite journal}}</code>: </span><span class="cs1-visible-error citation-comment">Cite journal requires <code class="cs1-code">|journal=</code> (help)</span></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text">Monin, pp.3-4</span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><cite id="CITEREFUttingReeves2001" class="citation journal cs1">Utting, Mark; Reeves, Steve (August 31, 2001). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.223">"Teaching formal methods lite via testing"</a></span>. <i>Software Testing, Verification and Reliability</i>. <b>11</b> (3): <span class="nowrap">181–</span>195. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1002%2Fstvr.223">10.1002/stvr.223</a>.</cite></span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><cite id="CITEREFBackus1959" class="citation conference cs1">Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". <i>Proceedings of the International Conference on Information Processing</i>. UNESCO.</cite></span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><a href="Donald_Knuth" title="Donald Knuth">Knuth, Donald E.</a> (1964), Backus Normal Form vs Backus Naur Form. <i><a href="Communications_of_the_ACM" title="Communications of the ACM">Communications of the ACM</a></i>, 7(12):735–736.</span>

</li>

<li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text"><cite id="CITEREFO'HearnTennent1997" class="citation book cs1">O'Hearn, Peter W.; Tennent, Robert D. (1997). <i>Algol-like Languages</i>.</cite></span>

</li>

<li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><cite id="CITEREFGulwaniPolozovSingh2017" class="citation journal cs1">Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh (2017). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://www.nowpublishers.com/article/Details/PGL-010">"Program Synthesis"</a></span>. <i>Foundations and Trends in Programming Languages</i>. <b>4</b> (<span class="nowrap">1–</span>2): <span class="nowrap">1–</span>119. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1561%2F2500000010">10.1561/2500000010</a>.</cite></span>

</li>

<li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text">A. Cortesi and M. Zanioli, <a rel="nofollow" class="external text" href="http://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf">Widening and Narrowing Operators for Abstract Interpretation</a>. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/1477-8424">1477-8424</a> (2011).</span>

</li>

<li id="cite_note-10"><span class="mw-cite-backlink"><b><a href="#cite_ref-10">^</a></b></span> <span class="reference-text"><cite id="CITEREFBjørnerHenson2008" class="citation book cs1">Bjørner, Dines; Henson, Martin C. (2008). <i>Logics of Specification Languages</i>. pp. <span class="nowrap">VII–</span>XI.</cite></span>

</li>

<li id="cite_note-11"><span class="mw-cite-backlink"><b><a href="#cite_ref-11">^</a></b></span> <span class="reference-text"><cite id="CITEREFBryant2018" class="citation book cs1">Bryant, Randal E. (2018). "Binary Decision Diagrams". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). <i>Handbook of Model Checking</i>. p. 191.</cite></span>

</li>

<li id="cite_note-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-12">^</a></b></span> <span class="reference-text"><cite id="CITEREFChakiGurfinkel2018" class="citation book cs1">Chaki, Sagar; Gurfinkel, Arie (2018). "BDD-Based Symbolic Model Checking". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). <i>Handbook of Model Checking</i>. p. 191.</cite></span>

</li>

<li id="cite_note-13"><span class="mw-cite-backlink"><b><a href="#cite_ref-13">^</a></b></span> <span class="reference-text"><cite id="CITEREFPrasadBiereGupta2005" class="citation journal cs1">Prasad, Mukul R; Biere, Armin; Gupta, Aarti (January 25, 2005). "A survey of recent advances in SAT-based formal verification". <i>International Journal on Software Tools for Technology Transfer</i>. <b>7</b> (2): <span class="nowrap">156–</span>173. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10009-004-0183-4">10.1007/s10009-004-0183-4</a>.</cite></span>

</li>

<li id="cite_note-14"><span class="mw-cite-backlink"><b><a href="#cite_ref-14">^</a></b></span> <span class="reference-text"><cite id="CITEREFBjørnerGramOestRystrøm2011" class="citation book cs1">Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). <i>History of Nordic Computing 3: IFIP Advances in Information and Communication Technology</i>. Springer. pp. <span class="nowrap">350–</span>359.</cite></span>

</li>

<li id="cite_note-15"><span class="mw-cite-backlink"><b><a href="#cite_ref-15">^</a></b></span> <span class="reference-text"><cite id="CITEREFBjørnerHavelund" class="citation conference cs1">Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". <a rel="nofollow" class="external text" href="http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf"><i>FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings</i></a> <span class="cs1-format">(PDF)</span>. Springer. pp. <span class="nowrap">42–</span>61.</cite></span>

</li>

<li id="cite_note-16"><span class="mw-cite-backlink"><b><a href="#cite_ref-16">^</a></b></span> <span class="reference-text">Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</span>

</li>

<li id="cite_note-17"><span class="mw-cite-backlink"><b><a href="#cite_ref-17">^</a></b></span> <span class="reference-text">Airborne Coordinated Conflict Resolution and Detection, <a rel="nofollow" class="external free" href="https://shemesh.larc.nasa.gov/people/cam/ACCoRD/">http://shemesh.larc.nasa.gov/people/cam/ACCoRD/</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20160305005830/http://shemesh.larc.nasa.gov/people/cam/ACCoRD/">Archived</a> 2016-03-05 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a></span>

</li>

<li id="cite_note-18"><span class="mw-cite-backlink"><b><a href="#cite_ref-18">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://www.atelierb.eu/en/">"Atelier B"</a>. <i>www.atelierb.eu</i>.</cite></span>

</li>

<li id="cite_note-19"><span class="mw-cite-backlink"><b><a href="#cite_ref-19">^</a></b></span> <span class="reference-text">C. T. Chou, P. K. Mannava, S. Park, "<a rel="nofollow" class="external text" href="https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf">A simple method for parameterized verification of cache coherence protocols</a>", Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</span>

</li>

<li id="cite_note-20"><span class="mw-cite-backlink"><b><a href="#cite_ref-20">^</a></b></span> <span class="reference-text">Formal Verification in Intel Core i7 Processor Execution Engine Validation, <a rel="nofollow" class="external free" href="http://cps-vo.org/node/1371">http://cps-vo.org/node/1371</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20150503222301/http://cps-vo.org/node/1371">Archived</a> 2015-05-03 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>, accessed at September 13, 2013.</span>

</li>

<li id="cite_note-21"><span class="mw-cite-backlink"><b><a href="#cite_ref-21">^</a></b></span> <span class="reference-text">J. Grundy, "Verified optimizations for the Intel IA-64 architecture", In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</span>

</li>

<li id="cite_note-22"><span class="mw-cite-backlink"><b><a href="#cite_ref-22">^</a></b></span> <span class="reference-text">E. Seligman, I. Yarom, "<a rel="nofollow" class="external text" href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf">Best known methods for using Cadence Conformal LEC</a>", at Intel.</span>

</li>

<li id="cite_note-23"><span class="mw-cite-backlink"><b><a href="#cite_ref-23">^</a></b></span> <span class="reference-text">C. Eisner, A. Nahir, K. Yorav, "<a rel="nofollow" class="external text" href="ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449">Functional verification of power gated designs by compositional reasoning</a>", Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</span>

</li>

<li id="cite_note-24"><span class="mw-cite-backlink"><b><a href="#cite_ref-24">^</a></b></span> <span class="reference-text">P. C. Attie, H. Chockler, "<a rel="nofollow" class="external text" href="https://core.ac.uk/download/pdf/82434920.pdf">Automatic verification of fault-tolerant register emulations</a>", Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</span>

</li>

<li id="cite_note-25"><span class="mw-cite-backlink"><b><a href="#cite_ref-25">^</a></b></span> <span class="reference-text">K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "<a rel="nofollow" class="external text" href="https://ieeexplore.ieee.org/abstract/document/5756329/">Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems</a>", IBM Journal of Research and Development, vol. 55, no 3.</span>

</li>

<li id="cite_note-26"><span class="mw-cite-backlink"><b><a href="#cite_ref-26">^</a></b></span> <span class="reference-text"><cite class="citation book cs1"><i>X2R-2, deliverable D5.1</i>.</cite></span>

</li>

<li id="cite_note-27"><span class="mw-cite-backlink"><b><a href="#cite_ref-27">^</a></b></span> <span class="reference-text"><a href="Daniel_Jackson_(computer_scientist)" title="Daniel Jackson (computer scientist)">Daniel Jackson</a> and <a href="Jeannette_Wing" title="Jeannette Wing">Jeannette Wing</a>, <a rel="nofollow" class="external text" href="http://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html">"Lightweight Formal Methods"</a>, <i>IEEE Computer</i>, April 1996</span>

</li>

<li id="cite_note-28"><span class="mw-cite-backlink"><b><a href="#cite_ref-28">^</a></b></span> <span class="reference-text">Vinu George and Rayford Vaughn, <a rel="nofollow" class="external text" href="http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html">"Application of Lightweight Formal Methods in Requirement Engineering"</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20060301022259/http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html">Archived</a> 2006-03-01 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>, <i>Crosstalk: The Journal of Defense Software Engineering</i>, January 2003</span>

</li>

<li id="cite_note-29"><span class="mw-cite-backlink"><b><a href="#cite_ref-29">^</a></b></span> <span class="reference-text">Daniel Jackson, <a rel="nofollow" class="external text" href="http://people.csail.mit.edu/dnj/publications/alloy-journal.pdf">"Alloy: A Lightweight Object Modelling Notation"</a>, <i>ACM Transactions on Software Engineering and Methodology (TOSEM)</i>, Volume 11, Issue 2 (April 2002), pp. 256-290</span>

</li>

<li id="cite_note-30"><span class="mw-cite-backlink"><b><a href="#cite_ref-30">^</a></b></span> <span class="reference-text">Richard Denney, <i>Succeeding with Use Cases: Working Smart to Deliver Quality</i>, Addison-Wesley Professional Publishing, 2005, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-321-31643-6</bdi>.</span>

</li>

<li id="cite_note-31"><span class="mw-cite-backlink"><b><a href="#cite_ref-31">^</a></b></span> <span class="reference-text">Sten Agerholm and Peter G. Larsen, <a rel="nofollow" class="external text" href="http://home0.inet.tele.dk/pgl/fmtrends98.pdf">"A Lightweight Approach to Formal Methods"</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20060309041943/http://home0.inet.tele.dk/pgl/fmtrends98.pdf">Archived</a> 2006-03-09 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a>, In <i>Proceedings of the International Workshop on Current Trends in Applied Formal Methods</i>, Boppard, Germany, Springer-Verlag, October 1998</span>

</li>

<li id="cite_note-32"><span class="mw-cite-backlink"><b><a href="#cite_ref-32">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="http://esbmc.org/">"ESBMC"</a>. <i>esbmc.org</i>.</cite></span>

</li>

<li id="cite_note-33"><span class="mw-cite-backlink"><b><a href="#cite_ref-33">^</a></b></span> <span class="reference-text"><cite id="CITEREFBartocciBeyerBlackFedyukovich2019" class="citation book cs1">Bartocci, Ezio; Beyer, Dirk; Black, Paul E.; Fedyukovich, Grigory; Garavel, Hubert; Hartmanns, Arnd; Huisman, Marieke; Kordon, Fabrice; Nagele, Julian; Sighireanu, Mihaela; Steffen, Bernhard; Suda, Martin; Sutcliffe, Geoff; Weber, Tjark; Yamada, Akihisa (2019). "TOOLympics 2019: An Overview of Competitions in Formal Methods". In Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (eds.). <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. <span class="nowrap">3–</span>24. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-17502-3_1">10.1007/978-3-030-17502-3_1</a></span>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-030-17502-3</bdi>.</cite></span>

</li>

<li id="cite_note-34"><span class="mw-cite-backlink"><b><a href="#cite_ref-34">^</a></b></span> <span class="reference-text"><cite id="CITEREFFroleyksHeuleIserJärvisalo2021" class="citation journal cs1">Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martin (2021-12-01). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.artint.2021.103572">"SAT Competition 2020"</a>. <i>Artificial Intelligence</i>. <b>301</b>: 103572. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.artint.2021.103572">10.1016/j.artint.2021.103572</a></span>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0004-3702">0004-3702</a>.</cite></span>

</li>

<li id="cite_note-35"><span class="mw-cite-backlink"><b><a href="#cite_ref-35">^</a></b></span> <span class="reference-text"><cite id="CITEREFCornejo2021" class="citation book cs1">Cornejo, César (2021-01-27). <a rel="nofollow" class="external text" href="https://doi.org/10.1145/3324884.3415285">"SAT-based arithmetic support for alloy"</a>. <i>Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering</i>. ASE '20. New York, NY, USA: Association for Computing Machinery. pp. <span class="nowrap">1161–</span>1163. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145%2F3324884.3415285">10.1145/3324884.3415285</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4503-6768-4</bdi>.</cite></span>

</li>

<li id="cite_note-36"><span class="mw-cite-backlink"><b><a href="#cite_ref-36">^</a></b></span> <span class="reference-text"><cite id="CITEREFBarrettDetersde_MouraOliveras2013" class="citation journal cs1">Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron (2013-03-01). <span class="id-lock-subscription" title="Paid subscription required"><a rel="nofollow" class="external text" href="https://doi.org/10.1007/s10817-012-9246-5">"6 Years of SMT-COMP"</a></span>. <i>Journal of Automated Reasoning</i>. <b>50</b> (3): <span class="nowrap">243–</span>277. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10817-012-9246-5">10.1007/s10817-012-9246-5</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/1573-0670">1573-0670</a>.</cite></span>

</li>

<li id="cite_note-37"><span class="mw-cite-backlink"><b><a href="#cite_ref-37">^</a></b></span> <span class="reference-text"><cite id="CITEREFFedyukovichRümmer2021" class="citation journal cs1">Fedyukovich, Grigory; Rümmer, Philipp (2021-09-13). <a rel="nofollow" class="external text" href="https://doi.org/10.4204%2FEPTCS.344.7">"Competition Report: CHC-COMP-21"</a>. <i>Electronic Proceedings in Theoretical Computer Science</i>. <b>344</b>: <span class="nowrap">91–</span>108. <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/2008.02939">2008.02939</a></span>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.4204%2FEPTCS.344.7">10.4204/EPTCS.344.7</a></span>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/2075-2180">2075-2180</a>.</cite></span>

</li>

<li id="cite_note-38"><span class="mw-cite-backlink"><b><a href="#cite_ref-38">^</a></b></span> <span class="reference-text"><cite id="CITEREFShuklaBierePulinaSeidl2019" class="citation book cs1">Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (November 2019). <a rel="nofollow" class="external text" href="https://ieeexplore.ieee.org/document/8995437">"A Survey on Applications of Quantified Boolean Formulas"</a>. <i>2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI)</i>. IEEE. pp. <span class="nowrap">78–</span>84. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FICTAI.2019.00020">10.1109/ICTAI.2019.00020</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-7281-3798-8</bdi>.</cite></span>

</li>

<li id="cite_note-39"><span class="mw-cite-backlink"><b><a href="#cite_ref-39">^</a></b></span> <span class="reference-text"><cite id="CITEREFPulinaSeidl2019" class="citation journal cs1">Pulina, Luca; Seidl, Martina (2019-09-01). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.artint.2019.04.002">"The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)"</a>. <i>Artificial Intelligence</i>. <b>274</b>: <span class="nowrap">224–</span>248. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.artint.2019.04.002">10.1016/j.artint.2019.04.002</a></span>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0004-3702">0004-3702</a>.</cite></span>

</li>

<li id="cite_note-40"><span class="mw-cite-backlink"><b><a href="#cite_ref-40">^</a></b></span> <span class="reference-text"><cite id="CITEREFBeyer2022" class="citation book cs1">Beyer, Dirk (2022). "Progress on Software Verification: SV-COMP 2022". In Fisman, Dana; Rosu, Grigore (eds.). <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Lecture Notes in Computer Science. Vol. 13244. Cham: Springer International Publishing. pp. <span class="nowrap">375–</span>402. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-99527-0_20">10.1007/978-3-030-99527-0_20</a></span>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-030-99527-0</bdi>.</cite></span>

</li>

<li id="cite_note-41"><span class="mw-cite-backlink"><b><a href="#cite_ref-41">^</a></b></span> <span class="reference-text"><cite id="CITEREFAlurFismanSinghSolar-Lezama2017" class="citation journal cs1">Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). <a rel="nofollow" class="external text" href="https://doi.org/10.4204%2FEPTCS.260.9">"SyGuS-Comp 2017: Results and Analysis"</a>. <i>Electronic Proceedings in Theoretical Computer Science</i>. <b>260</b>: <span class="nowrap">97–</span>115. <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/1611.07627">1611.07627</a></span>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.4204%2FEPTCS.260.9">10.4204/EPTCS.260.9</a></span>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/2075-2180">2075-2180</a>.</cite></span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .refbegin{margin-bottom:0.5em}.mw-parser-output .refbegin-hanging-indents>ul{margin-left:0}.mw-parser-output .refbegin-hanging-indents>ul>li{margin-left:0;padding-left:3.2em;text-indent:-3.2em}.mw-parser-output .refbegin-hanging-indents ul,.mw-parser-output .refbegin-hanging-indents ul li{list-style:none}@media(max-width:720px){.mw-parser-output .refbegin-hanging-indents>ul>li{padding-left:1.6em;text-indent:-1.6em}}.mw-parser-output .refbegin-columns{margin-top:0.3em}.mw-parser-output .refbegin-columns ul{margin-top:0}.mw-parser-output .refbegin-columns li{page-break-inside:avoid;break-inside:avoid-column}@media screen{.mw-parser-output .refbegin{font-size:90%}}

/* end https://en.wikipedia.org/ */

</style><div class="refbegin" style="">

<ul><li><a href="Jonathan_P._Bowen" class="mw-redirect" title="Jonathan P. Bowen">Jonathan P. Bowen</a> and Michael G. Hinchey, <i>Formal Methods</i>. In Allen B. Tucker, Jr. (ed.), <i>Computer Science Handbook</i>, 2nd edition, Section XI, <i>Software Engineering</i>, Chapter 106, pages 106-1 – 106-25, <a href="Chapman_%26_Hall" title="Chapman & Hall">Chapman & Hall</a> / <a href="CRC_Press" title="CRC Press">CRC Press</a>, <a href="Association_for_Computing_Machinery" title="Association for Computing Machinery">Association for Computing Machinery</a>, 2004.</li>

<li>Hubert Garavel (editor) and Susanne Graf. <a rel="nofollow" class="external text" href="https://www.bsi.bund.de/SharedDocs/DE/Publikationen/Studien/formal_methods_study_875/study_875.html"><i>Formal Methods for Safe and Secure Computer Systems</i></a>. <a href="Federal_Office_for_Information_Security" title="Federal Office for Information Security">Bundesamt für Sicherheit in der Informationstechnik</a>, BSI study 875, Bonn, Germany, December 2013.</li>

<li><cite id="CITEREFGaravelter_Beekvan_de_Pol2020" class="citation book cs1">Garavel, Hubert; ter Beek, Maurice H.; van de Pol, Jaco (29 August 2020). "The 2020 Expert Survey on Formal Methods". <a rel="nofollow" class="external text" href="https://hal.inria.fr/hal-03082818/file/Garavel-terBeek-vandePol-20.pdf"><i>Formal Methods for Industrial Critical Systems: 25 International Conference, FMICS 2020</i></a> <span class="cs1-format">(PDF)</span>. <a href="Lecture_Notes_in_Computer_Science" title="Lecture Notes in Computer Science">Lecture Notes in Computer Science</a> (LNCS). Vol. 12327. <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer</a>. pp. <span class="nowrap">3–</span>69. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-030-58298-2_1">10.1007/978-3-030-58298-2_1</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-030-58297-5</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:221381022">221381022</a>.</cite>* Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, <i>Formal Methods</i>. In Philip A. Laplante (ed.), <i>Encyclopedia of Software Engineering</i>, <a href="Taylor_%26_Francis" title="Taylor & Francis">Taylor & Francis</a>, 2010, pages 308–320.</li>

<li><a href="Marieke_Huisman" title="Marieke Huisman">Marieke Huisman</a>, Dilian Gurov, and Alexander Malkis, <a rel="nofollow" class="external text" href="http://arxiv.org/abs/2002.07279"><i>Formal Methods: From Academia to Industrial Practice – A Travel Guide</i></a>, arXiv:2002.07279, 2020.</li>

<li><cite id="CITEREFGleirscherMarmsoler2020" class="citation journal cs1">Gleirscher, Mario; Marmsoler, Diego (9 September 2020). <a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10664-020-09836-5">"Formal methods in dependable systems engineering: a survey of professionals from Europe and North America"</a>. <i>Empirical Software Engineering</i>. <b>25</b> (6). <a href="Springer_Nature" title="Springer Nature">Springer Nature</a>: <span class="nowrap">4473–</span>4546. <a href="ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/1812.08815">1812.08815</a></span>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10664-020-09836-5">10.1007/s10664-020-09836-5</a></span>.</cite></li>

<li>Jean François Monin and <a href="Michael_G._Hinchey" class="mw-redirect" title="Michael G. Hinchey">Michael G. Hinchey</a>, <i>Understanding formal methods</i>, <a href="Springer-Verlag" class="mw-redirect" title="Springer-Verlag">Springer</a>, 2003, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>1-85233-247-6</bdi>.</li></ul>

</div>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><a rel="nofollow" class="external text" href="http://www.fmeurope.org/">Formal Methods Europe</a> (FME)</li>

<li><a rel="nofollow" class="external text" href="https://formalmethods.wikia.org/">Formal Methods Wiki</a></li>

<li><a rel="nofollow" class="external text" href="http://foldoc.org/formal+methods">Formal methods</a> from <a rel="nofollow" class="external text" href="https://foldoc.org/">Foldoc</a></li></ul>

<dl><dt>Archival material</dt></dl>

<ul><li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20130404202524/http://academic.research.microsoft.com/Keyword/14916">Formal method</a> keyword on <a href="Microsoft_Academic_Search" title="Microsoft Academic Search">Microsoft Academic Search</a> via <a href="Archive.org" class="mw-redirect" title="Archive.org">Archive.org</a></li>

<li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20170713233230/http://www.fm4industry.org/index.php/Evidence_on_Formal_Methods_uses_and_impact_on_Industry">Evidence on Formal Methods uses and impact on Industry</a> supported by the <a rel="nofollow" class="external text" href="http://www.deploy-project.eu">DEPLOY</a> <a rel="nofollow" class="external text" href="https://web.archive.org/web/20120608063125/http://www.deploy-project.eu/">Archived</a> 2012-06-08 at the <a href="Wayback_Machine" title="Wayback Machine">Wayback Machine</a> project (EU FP7) in <a href="Archive.org" class="mw-redirect" title="Archive.org">Archive.org</a></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Computer_science1050" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Computer_science1050" style="font-size:114%;margin:0 4em"><a href="Computer_science" title="Computer science">Computer science</a></div></th></tr><tr><td class="navbox-abovebelow" colspan="2"><div>Note: This template roughly follows the 2012 <a href="ACM_Computing_Classification_System" title="ACM Computing Classification System">ACM Computing Classification System</a>.</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computer_hardware" title="Computer hardware">Hardware</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Printed_circuit_board" title="Printed circuit board">Printed circuit board</a></li>

<li><a href="Peripheral" title="Peripheral">Peripheral</a></li>

<li><a href="Integrated_circuit" title="Integrated circuit">Integrated circuit</a></li>

<li><a href="Very-large-scale_integration" title="Very-large-scale integration">Very-large-scale integration</a></li>

<li><a href="System_on_a_chip" title="System on a chip">System on a chip</a> (SoC)</li>

<li><a href="Green_computing" title="Green computing">Energy consumption</a> (green computing)</li>

<li><a href="Electronic_design_automation" title="Electronic design automation">Electronic design automation</a></li>

<li><a href="Hardware_acceleration" title="Hardware acceleration">Hardware acceleration</a></li>

<li><a href="Processor_(computing)" title="Processor (computing)">Processor</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Computer systems organization</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Computer_architecture" title="Computer architecture">Computer architecture</a></li>

<li><a href="Computational_complexity" title="Computational complexity">Computational complexity</a></li>

<li><a href="Dependability" title="Dependability">Dependability</a></li>

<li><a href="Embedded_system" title="Embedded system">Embedded system</a></li>

<li><a href="Real-time_computing" title="Real-time computing">Real-time computing</a></li>

<li><a href="Cyber-physical_system" title="Cyber-physical system">Cyber-physical system</a></li>

<li><a href="Fault_tolerance" title="Fault tolerance">Fault tolerance</a></li>

<li><a href="Wireless_sensor_network" title="Wireless sensor network">Wireless sensor network</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computer_network" title="Computer network">Networks</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Network_architecture" title="Network architecture">Network architecture</a></li>

<li><a href="Communication_protocol" title="Communication protocol">Network protocol</a></li>

<li><a href="Networking_hardware" title="Networking hardware">Network components</a></li>

<li><a href="Network_scheduler" title="Network scheduler">Network scheduler</a></li>

<li><a href="Network_performance" title="Network performance">Network performance evaluation</a></li>

<li><a href="Network_service" title="Network service">Network service</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software organization</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Interpreter_(computing)" title="Interpreter (computing)">Interpreter</a></li>

<li><a href="Middleware" title="Middleware">Middleware</a></li>

<li><a href="Virtual_machine" title="Virtual machine">Virtual machine</a></li>

<li><a href="Operating_system" title="Operating system">Operating system</a></li>

<li><a href="Software_quality" title="Software quality">Software quality</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Programming_language_theory" title="Programming language theory">Software notations</a> and <a href="Programming_tool" title="Programming tool">tools</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Programming_paradigm" title="Programming paradigm">Programming paradigm</a></li>

<li><a href="Programming_language" title="Programming language">Programming language</a></li>

<li><a href="Compiler_construction" class="mw-redirect" title="Compiler construction">Compiler</a></li>

<li><a href="Domain-specific_language" title="Domain-specific language">Domain-specific language</a></li>

<li><a href="Modeling_language" title="Modeling language">Modeling language</a></li>

<li><a href="Software_framework" title="Software framework">Software framework</a></li>

<li><a href="Integrated_development_environment" title="Integrated development environment">Integrated development environment</a></li>

<li><a href="Software_configuration_management" title="Software configuration management">Software configuration management</a></li>

<li><a href="Library_(computing)" title="Library (computing)">Software library</a></li>

<li><a href="Software_repository" title="Software repository">Software repository</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Software_development" title="Software development">Software development</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Control_flow" title="Control flow">Control variable</a></li>

<li><a href="Software_development_process" title="Software development process">Software development process</a></li>

<li><a href="Requirements_analysis" title="Requirements analysis">Requirements analysis</a></li>

<li><a href="Software_design" title="Software design">Software design</a></li>

<li><a href="Software_construction" title="Software construction">Software construction</a></li>

<li><a href="Software_deployment" title="Software deployment">Software deployment</a></li>

<li><a href="Software_engineering" title="Software engineering">Software engineering</a></li>

<li><a href="Software_maintenance" title="Software maintenance">Software maintenance</a></li>

<li><a href="Programming_team" title="Programming team">Programming team</a></li>

<li><a href="Open-source_software" title="Open-source software">Open-source model</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Theory_of_computation" title="Theory of computation">Theory of computation</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Model_of_computation" title="Model of computation">Model of computation</a>

<ul><li><a href="Stochastic_computing" title="Stochastic computing">Stochastic</a></li></ul></li>

<li><a href="Formal_language" title="Formal language">Formal language</a></li>

<li><a href="Automata_theory" title="Automata theory">Automata theory</a></li>

<li><a href="Computability_theory" title="Computability theory">Computability theory</a></li>

<li><a href="Computational_complexity_theory" title="Computational complexity theory">Computational complexity theory</a></li>

<li><a href="Logic_in_computer_science" title="Logic in computer science">Logic</a></li>

<li><a href="Semantics_(computer_science)" title="Semantics (computer science)">Semantics</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Algorithm" title="Algorithm">Algorithms</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Algorithm_design" class="mw-redirect" title="Algorithm design">Algorithm design</a></li>

<li><a href="Analysis_of_algorithms" title="Analysis of algorithms">Analysis of algorithms</a></li>

<li><a href="Algorithmic_efficiency" title="Algorithmic efficiency">Algorithmic efficiency</a></li>

<li><a href="Randomized_algorithm" title="Randomized algorithm">Randomized algorithm</a></li>

<li><a href="Computational_geometry" title="Computational geometry">Computational geometry</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Mathematics of <a href="Computing" title="Computing">computing</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Discrete_mathematics" title="Discrete mathematics">Discrete mathematics</a></li>

<li><a href="Probability" title="Probability">Probability</a></li>

<li><a href="Statistics" title="Statistics">Statistics</a></li>

<li><a href="Mathematical_software" title="Mathematical software">Mathematical software</a></li>

<li><a href="Information_theory" title="Information theory">Information theory</a></li>

<li><a href="Mathematical_analysis" title="Mathematical analysis">Mathematical analysis</a></li>

<li><a href="Numerical_analysis" title="Numerical analysis">Numerical analysis</a></li>

<li><a href="Theoretical_computer_science" title="Theoretical computer science">Theoretical computer science</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Information_system" title="Information system">Information systems</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Database" title="Database">Database management system</a></li>

<li><a href="Computer_data_storage" title="Computer data storage">Information storage systems</a></li>

<li><a href="Enterprise_information_system" title="Enterprise information system">Enterprise information system</a></li>

<li><a href="Social_software" title="Social software">Social information systems</a></li>

<li><a href="Geographic_information_system" title="Geographic information system">Geographic information system</a></li>

<li><a href="Decision_support_system" title="Decision support system">Decision support system</a></li>

<li><a href="Industrial_process_control" title="Industrial process control">Process control system</a></li>

<li><a href="Multimedia_database" title="Multimedia database">Multimedia information system</a></li>

<li><a href="Data_mining" title="Data mining">Data mining</a></li>

<li><a href="Digital_library" title="Digital library">Digital library</a></li>

<li><a href="Computing_platform" title="Computing platform">Computing platform</a></li>

<li><a href="Digital_marketing" title="Digital marketing">Digital marketing</a></li>

<li><a href="World_Wide_Web" title="World Wide Web">World Wide Web</a></li>

<li><a href="Information_retrieval" title="Information retrieval">Information retrieval</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computer_security" title="Computer security">Security</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Cryptography" title="Cryptography">Cryptography</a></li>

<li><a href="Security_hacker" title="Security hacker">Security hacker</a></li>

<li><a href="Security_service_(telecommunication)" title="Security service (telecommunication)">Security services</a></li>

<li><a href="Intrusion_detection_system" title="Intrusion detection system">Intrusion detection system</a></li>

<li><a href="Hardware_security" title="Hardware security">Hardware security</a></li>

<li><a href="Network_security" title="Network security">Network security</a></li>

<li><a href="Information_security" title="Information security">Information security</a></li>

<li><a href="Application_security" title="Application security">Application security</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a class="external text external" href="https://en.wikipedia.org/wiki/Human-centered_computing">Human–centered computing</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Interaction_design" title="Interaction design">Interaction design</a></li>

<li><a href="Augmented_reality" title="Augmented reality">Augmented reality</a></li>

<li><a href="Virtual_reality" title="Virtual reality">Virtual reality</a></li>

<li><a href="Social_computing" title="Social computing">Social computing</a></li>

<li><a href="Ubiquitous_computing" title="Ubiquitous computing">Ubiquitous computing</a></li>

<li><a href="Visualization_(graphics)" title="Visualization (graphics)">Visualization</a></li>

<li><a href="Computer_accessibility" title="Computer accessibility">Accessibility</a></li>

<li><a href="Human%E2%80%93computer_interaction" title="Human–computer interaction">Human–computer interaction</a></li>

<li><a href="Mobile_computing" title="Mobile computing">Mobile computing</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Concurrency_(computer_science)" title="Concurrency (computer science)">Concurrency</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Concurrent_computing" title="Concurrent computing">Concurrent computing</a></li>

<li><a href="Parallel_computing" title="Parallel computing">Parallel computing</a></li>

<li><a href="Distributed_computing" title="Distributed computing">Distributed computing</a></li>

<li><a href="Multithreading_(computer_architecture)" title="Multithreading (computer architecture)">Multithreading</a></li>

<li><a href="Multiprocessing" title="Multiprocessing">Multiprocessing</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Artificial_intelligence" title="Artificial intelligence">Artificial intelligence</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Natural_language_processing" title="Natural language processing">Natural language processing</a></li>

<li><a href="Knowledge_representation_and_reasoning" title="Knowledge representation and reasoning">Knowledge representation and reasoning</a></li>

<li><a href="Computer_vision" title="Computer vision">Computer vision</a></li>

<li><a href="Automated_planning_and_scheduling" title="Automated planning and scheduling">Automated planning and scheduling</a></li>

<li><a href="Mathematical_optimization" title="Mathematical optimization">Search methodology</a></li>

<li><a href="Control_theory" title="Control theory">Control method</a></li>

<li><a href="Philosophy_of_artificial_intelligence" title="Philosophy of artificial intelligence">Philosophy of artificial intelligence</a></li>

<li><a href="Distributed_artificial_intelligence" title="Distributed artificial intelligence">Distributed artificial intelligence</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Machine_learning" title="Machine learning">Machine learning</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Supervised_learning" title="Supervised learning">Supervised learning</a></li>

<li><a href="Unsupervised_learning" title="Unsupervised learning">Unsupervised learning</a></li>

<li><a href="Reinforcement_learning" title="Reinforcement learning">Reinforcement learning</a></li>

<li><a href="Multi-task_learning" title="Multi-task learning">Multi-task learning</a></li>

<li><a href="Cross-validation_(statistics)" title="Cross-validation (statistics)">Cross-validation</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Computer_graphics" title="Computer graphics">Graphics</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Computer_animation" title="Computer animation">Animation</a></li>

<li><a href="Rendering_(computer_graphics)" title="Rendering (computer graphics)">Rendering</a></li>

<li><a href="Photograph_manipulation" title="Photograph manipulation">Photograph manipulation</a></li>

<li><a href="Graphics_processing_unit" title="Graphics processing unit">Graphics processing unit</a></li>

<li><a href="Image_compression" title="Image compression">Image compression</a></li>

<li><a href="Solid_modeling" title="Solid modeling">Solid modeling</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Applied computing</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Quantum_computing" title="Quantum computing">Quantum computing</a></li>

<li><a href="E-commerce" title="E-commerce">E-commerce</a></li>

<li><a href="Enterprise_software" title="Enterprise software">Enterprise software</a></li>

<li><a href="Computational_mathematics" title="Computational mathematics">Computational mathematics</a></li>

<li><a href="Computational_physics" title="Computational physics">Computational physics</a></li>

<li><a href="Computational_chemistry" title="Computational chemistry">Computational chemistry</a></li>

<li><a href="Computational_biology" title="Computational biology">Computational biology</a></li>

<li><a href="Computational_social_science" title="Computational social science">Computational social science</a></li>

<li><a href="Computational_engineering" title="Computational engineering">Computational engineering</a></li>

<li>Differentiable computing</li>

<li><a href="Health_informatics" title="Health informatics">Computational healthcare</a></li>

<li><a href="Digital_art" title="Digital art">Digital art</a></li>

<li><a href="Electronic_publishing" title="Electronic publishing">Electronic publishing</a></li>

<li><a href="Cyberwarfare" title="Cyberwarfare">Cyberwarfare</a></li>

<li><a href="Electronic_voting" title="Electronic voting">Electronic voting</a></li>

<li><a href="Video_game" title="Video game">Video games</a></li>

<li><a href="Word_processor" title="Word processor">Word processing</a></li>

<li><a href="Operations_research" title="Operations research">Operations research</a></li>

<li><a href="Educational_technology" title="Educational technology">Educational technology</a></li>

<li><a href="Document_management_system" title="Document management system">Document management</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li>

<li><span class="noviewer" typeof="mw:File"><span title="Outline"></span></span> <a href="Outline_of_computer_science" title="Outline of computer science">Outline</a></li>

<li><span class="noviewer" typeof="mw:File"><span></span></span> Glossaries</li></ul>

</div></td></tr></tbody></table></div>

<div class="navbox-styles"></div><div role="navigation" class="navbox" aria-labelledby="Software_engineering336" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Software_engineering336" style="font-size:114%;margin:0 4em"><a href="Software_engineering" title="Software engineering">Software engineering</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Fields</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Computer_programming" title="Computer programming">Computer programming</a></li>

<li><a href="DevOps" title="DevOps">DevOps</a></li>

<li><a href="Empirical_software_engineering" title="Empirical software engineering">Empirical software engineering</a></li>

<li><a href="Experimental_software_engineering" title="Experimental software engineering">Experimental software engineering</a></li>

<li><a href="Requirements_engineering" title="Requirements engineering">Requirements engineering</a></li>

<li><a href="Search-based_software_engineering" title="Search-based software engineering">Search-based software engineering</a></li>

<li><a href="Site_reliability_engineering" title="Site reliability engineering">Site reliability engineering</a></li>

<li><a href="Social_software_engineering" title="Social software engineering">Social software engineering</a></li>

<li><a href="Software_deployment" title="Software deployment">Software deployment</a></li>

<li><a href="Software_design" title="Software design">Software design</a></li>

<li><a href="Software_maintenance" title="Software maintenance">Software maintenance</a></li>

<li><a href="Software_testing" title="Software testing">Software testing</a></li>

<li><a href="Systems_analysis" title="Systems analysis">Systems analysis</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Concepts</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Abstraction_(computer_science)" title="Abstraction (computer science)">Abstraction</a></li>

<li><a href="Computer_compatibility" title="Computer compatibility">Compatibility</a>

<ul><li><a href="Backward_compatibility" title="Backward compatibility">Backward compatibility</a></li>

<li><a href="Compatibility_layer" title="Compatibility layer">Compatibility layer</a></li>

<li><a href="Compatibility_mode" title="Compatibility mode">Compatibility mode</a></li>

<li><a href="Forward_compatibility" title="Forward compatibility">Forward compatibility</a></li>

<li><a href="Software_incompatibility" title="Software incompatibility">Software incompatibility</a></li></ul></li>

<li><a href="Component-based_software_engineering" title="Component-based software engineering">Component-based software engineering</a></li>

<li><a href="Data_modeling" title="Data modeling">Data modeling</a></li>

<li><a href="Enterprise_architecture" title="Enterprise architecture">Enterprise architecture</a></li>

<li><a href="Functional_specification" title="Functional specification">Functional specification</a></li>

<li><a href="Modeling_language" title="Modeling language">Modeling language</a></li>

<li><a href="Programming_paradigm" title="Programming paradigm">Programming paradigm</a></li>

<li><a href="Software" title="Software">Software</a></li>

<li><a href="Software_archaeology" title="Software archaeology">Software archaeology</a></li>

<li><a href="Software_architecture" title="Software architecture">Software architecture</a></li>

<li><a href="Software_configuration_management" title="Software configuration management">Software configuration management</a></li>

<li><a href="Software_development_process" title="Software development process">Software development process/methodology</a></li>

<li><a href="Software_quality" title="Software quality">Software quality</a></li>

<li><a href="Software_quality_assurance" title="Software quality assurance">Software quality assurance</a></li>

<li><a href="Software_system" title="Software system">Software system</a></li>

<li><a href="Software_verification_and_validation" title="Software verification and validation">Software verification and validation</a></li>

<li><a href="Structured_analysis" title="Structured analysis">Structured analysis</a>

<ul><li><a href="Essential_systems_analysis" title="Essential systems analysis">Essential analysis</a></li></ul></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Orientations</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Agile_software_development" title="Agile software development">Agile</a></li>

<li><a href="Aspect-oriented_programming" title="Aspect-oriented programming">Aspect-oriented</a></li>

<li><a href="Object-oriented_programming" title="Object-oriented programming">Object orientation</a></li>

<li><a href="Ontology_(information_science)" title="Ontology (information science)">Ontology</a></li>

<li><a href="Service-oriented_architecture" title="Service-oriented architecture">Service orientation</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Models</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Developmental</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Agile_software_development" title="Agile software development">Agile</a></li>

<li><a href="Executable_UML" title="Executable UML">Executable UML</a></li>

<li><a href="Incremental_build_model" title="Incremental build model">Incremental model</a></li>

<li><a href="Iterative_and_incremental_development" title="Iterative and incremental development">Iterative model</a></li>

<li><a href="Software_prototyping" title="Software prototyping">Prototype model</a></li>

<li><a href="Scrum_(software_development)" title="Scrum (software development)">Scrum</a></li>

<li><a href="Spiral_model" title="Spiral model">Spiral model</a></li>

<li><a href="V-model_(software_development)" title="V-model (software development)">V-model</a></li>

<li><a href="Waterfall_model" title="Waterfall model">Waterfall model</a></li>

<li><a href="Model-driven_engineering" title="Model-driven engineering">Model-driven engineering</a></li>

<li><a href="Round-trip_engineering" title="Round-trip engineering">Round-trip engineering</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="Data_model" title="Data model">Data model</a></li>

<li><a href="Entity%E2%80%93relationship_model" title="Entity–relationship model">ER model</a></li>

<li><a href="Function_model" title="Function model">Function model</a></li>

<li><a href="Information_model" title="Information model">Information model</a></li>

<li><a href="Metamodeling" title="Metamodeling">Metamodeling</a></li>

<li><a href="Object_model" title="Object model">Object model</a></li>

<li><a href="ISO/IEC_15504" title="ISO/IEC 15504">SPICE</a></li>

<li><a href="Systems_modeling" title="Systems modeling">Systems model</a></li>

<li><a href="View_model" title="View model">View model</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Languages</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="Systems_modeling_language" title="Systems modeling language">SysML</a></li>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Systems_design" title="Systems design">Systems design</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Software_requirements_specification" title="Software requirements specification"> Requirements</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Functional_requirement" title="Functional requirement">Functional requirement</a></li>

<li><a href="Non-functional_requirement" title="Non-functional requirement">Non-functional requirement</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Capacity_planning" title="Capacity planning"> Capacity</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Active_users" title="Active users"> Users</a></li>

<li><a href="Central_processing_units" class="mw-redirect" title="Central processing units"> Compute</a></li>

<li><a href="Computer_memory" title="Computer memory"> Memory</a></li>

<li><a href="Computer_data_storage" title="Computer data storage"> Storage</a></li>

<li><a href="Bandwidth_(computing)" title="Bandwidth (computing)"> Network</a></li>

<li><a href="Web_traffic" title="Web traffic">Web traffic</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Interface_(computing)" title="Interface (computing)"> Interface</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="GraphQL" title="GraphQL">GraphQL</a></li>

<li><a href="Webhook" title="Webhook">Webhook</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="High-level_design" title="High-level design">High-level design</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Client_(computing)" title="Client (computing)"> Client</a></li>

<li><a href="Load_balancing_(computing)" title="Load balancing (computing)"> Load balancing</a></li>

<li><a href="Application_server" title="Application server">Application server</a></li>

<li><a href="Message_queue" title="Message queue">Message queue</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="System_Integration" class="mw-redirect" title="System Integration"> Integration</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Vertical_integration" title="Vertical integration"> Vertical</a></li>

<li><a href="API_management" title="API management"> API Gateway</a></li>

<li><a href="Event_store" title="Event store"> Event Source</a></li>

<li><a href="Batch_processing" title="Batch processing"> Batch</a></li>

<li><a href="Stream_processing" title="Stream processing">Stream</a></li>

<li><a href="Orchestration_(computing)" title="Orchestration (computing)"> Orchestration</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Architectures" class="mw-redirect" title="Architectures">Architectures</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Monolithic_application" title="Monolithic application"> Monolithic</a></li>

<li><a href="Microservices" title="Microservices">Microservices</a></li>

<li><a href="Event-driven_architecture" title="Event-driven architecture"> Event-Driven</a></li>

<li><a href="Client%E2%80%93server_model" title="Client–server model"> Client–server</a></li>

<li><a href="Serverless_computing" title="Serverless computing"> Serverless</a></li>

<li><a href="Circuit_breaker_design_pattern" title="Circuit breaker design pattern"> Circuit breaker</a></li>

<li><a href="Rate_limiting" title="Rate limiting">Rate limiting</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Database" title="Database">Database</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Relational_database" title="Relational database"> Relational</a></li>

<li><a href="NoSQL" title="NoSQL">NoSQL</a></li>

<li><a href="Graph_database" title="Graph database"> Graph</a></li>

<li><a href="Key%E2%80%93value_database" title="Key–value database"> Key–value</a></li>

<li><a href="Time_series_database" title="Time series database"> Time series</a></li>

<li><a href="Data_orientation" title="Data orientation"> Column Oriented</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Systems_design" title="Systems design"> Principles</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Consistency_(database_systems)" title="Consistency (database systems)">Consistency</a></li>

<li><a href="Reliability_engineering" title="Reliability engineering">Reliability</a></li>

<li><a href="CAP_theorem" title="CAP theorem">CAP theorem</a></li>

<li><a href="Software_maintenance" title="Software maintenance"> Maintainability</a></li>

<li><a href="Computer_configuration" title="Computer configuration"> Configurability</a></li>

<li><a href="Modularity" title="Modularity">Modularity</a></li>

<li><a href="Durability_(database_systems)" title="Durability (database systems)"> Durability</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Scalability" title="Scalability">Scalability</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Service_statelessness_principle" title="Service statelessness principle"> Stateless</a></li>

<li><a href="Asynchronous_I/O" title="Asynchronous I/O">Asynchronous I/O</a></li>

<li><a href="Loose_coupling" title="Loose coupling">Loose coupling</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Availability" title="Availability">Availability</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Fault_tolerance" title="Fault tolerance">Fault tolerance</a></li>

<li><a href="Failover" title="Failover">Failover</a></li>

<li><a href="Single_point_of_failure" title="Single point of failure">Single point of failure</a></li>

<li><a href="Replication_(computing)" title="Replication (computing)"> Replication</a></li>

<li><a href="Consistent_hashing" title="Consistent hashing">Consistent hashing</a></li>

<li><a href="Circuit_breaker_design_pattern" title="Circuit breaker design pattern"> Circuit breaker</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Latency_(engineering)" title="Latency (engineering)">Latency</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Cache_(computing)" title="Cache (computing)"> Cache</a></li>

<li><a href="Shard_(database_architecture)" title="Shard (database architecture)"> Shard </a></li>

<li><a href="Database_index" title="Database index">Database index</a></li>

<li><a href="Cache_prefetching" title="Cache prefetching"> Pre-caching</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Computer_data_storage" title="Computer data storage"> Storage</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Object_storage" title="Object storage">Object storage</a></li>

<li><a href="Block-level_storage" title="Block-level storage"> Block storage</a></li></ul>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="Observability_(software)" title="Observability (software)"> Observability</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Logging_(computing)" title="Logging (computing)"> Logging</a></li>

<li><a href="Software_metric" title="Software metric"> Metrics</a></li>

<li><a href="Tracing_(software)" title="Tracing (software)"> Tracing </a></li>

<li><a href="Failure_rate" title="Failure rate"> Error rate </a></li>

<li><a href="Queries_per_second" title="Queries per second">Queries per second </a></li>

<li><a href="Notification_system" title="Notification system">Notification system</a></li>

<li><a href="Anomaly_detection" title="Anomaly detection">Anomaly detection</a></li></ul>

</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related fields</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="Computer_engineering" title="Computer engineering">Computer engineering</a></li>

<li><a href="Computer_science" title="Computer science">Computer science</a></li>

<li><a href="Information_science" title="Information science">Information science</a></li>

<li><a href="Project_management" title="Project management">Project management</a></li>

<li><a href="Risk_management" title="Risk management">Risk management</a></li>

<li><a href="Systems_engineering" title="Systems engineering">Systems engineering</a></li></ul>

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2" style="font-weight:bold;"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li>

<li><span class="noviewer" typeof="mw:File"><span title="Commons page"></span></span> <a href="https://commons.wikimedia.org/wiki/Category:Software_engineering" class="extiw external" title="commons:Category:Software engineering">Commons</a></li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-06-19" href="https://en.wikipedia.org/wiki/?title=Formal_methods&oldid=1296416147">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>